0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 185 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 210 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPOrderProof (⇔, 91 ms)
↳29 QDP
↳30 DependencyGraphProof (⇔, 0 ms)
↳31 QDP
↳32 UsableRulesProof (⇔, 0 ms)
↳33 QDP
↳34 QReductionProof (⇔, 0 ms)
↳35 QDP
↳36 QDPSizeChangeProof (⇔, 0 ms)
↳37 YES
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_GGA(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → LEA_IN_GG(T31, T32)
LEA_IN_GG(s(T45), s(T46)) → U1_GG(T45, T46, leA_in_gg(T45, T46))
LEA_IN_GG(s(T45), s(T46)) → LEA_IN_GG(T45, T46)
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_GGA(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → MERGEC_IN_GGA(T18, .(s(T32), T20), T22)
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_GGA(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(s(T60), T20), T22)
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_GGA(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(zero, T20), T22)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_GGA(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → GTB_IN_GG(T75, T77)
GTB_IN_GG(s(T93), s(T94)) → U2_GG(T93, T94, gtB_in_gg(T93, T94))
GTB_IN_GG(s(T93), s(T94)) → GTB_IN_GG(T93, T94)
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_GGA(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → MERGEC_IN_GGA(.(T75, T76), T78, T80)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_GGA(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → GTB_IN_GG(T123, T124)
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_GGA(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → MERGEC_IN_GGA(.(s(T123), T110), T112, T114)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_GGA(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEC_IN_GGA(.(s(T135), T110), T112, T114)
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_GGA(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → LEA_IN_GG(T31, T32)
LEA_IN_GG(s(T45), s(T46)) → U1_GG(T45, T46, leA_in_gg(T45, T46))
LEA_IN_GG(s(T45), s(T46)) → LEA_IN_GG(T45, T46)
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_GGA(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → MERGEC_IN_GGA(T18, .(s(T32), T20), T22)
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_GGA(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(s(T60), T20), T22)
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_GGA(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(zero, T20), T22)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_GGA(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → GTB_IN_GG(T75, T77)
GTB_IN_GG(s(T93), s(T94)) → U2_GG(T93, T94, gtB_in_gg(T93, T94))
GTB_IN_GG(s(T93), s(T94)) → GTB_IN_GG(T93, T94)
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_GGA(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → MERGEC_IN_GGA(.(T75, T76), T78, T80)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_GGA(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → GTB_IN_GG(T123, T124)
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_GGA(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → MERGEC_IN_GGA(.(s(T123), T110), T112, T114)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_GGA(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEC_IN_GGA(.(s(T135), T110), T112, T114)
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
GTB_IN_GG(s(T93), s(T94)) → GTB_IN_GG(T93, T94)
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
GTB_IN_GG(s(T93), s(T94)) → GTB_IN_GG(T93, T94)
GTB_IN_GG(s(T93), s(T94)) → GTB_IN_GG(T93, T94)
From the DPs we obtained the following set of size-change graphs:
LEA_IN_GG(s(T45), s(T46)) → LEA_IN_GG(T45, T46)
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
LEA_IN_GG(s(T45), s(T46)) → LEA_IN_GG(T45, T46)
LEA_IN_GG(s(T45), s(T46)) → LEA_IN_GG(T45, T46)
From the DPs we obtained the following set of size-change graphs:
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → MERGEC_IN_GGA(T18, .(s(T32), T20), T22)
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_GGA(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(s(T60), T20), T22)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_GGA(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → MERGEC_IN_GGA(.(T75, T76), T78, T80)
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(zero, T20), T22)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEC_IN_GGA(.(s(T135), T110), T112, T114)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_GGA(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → MERGEC_IN_GGA(.(s(T123), T110), T112, T114)
mergeC_in_gga(T5, [], T5) → mergeC_out_gga(T5, [], T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga([], T11, T11) → mergeC_out_gga([], T11, T11)
mergeC_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_gga(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_gga(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → U4_gga(T31, T18, T32, T20, T22, mergeC_in_gga(T18, .(s(T32), T20), T22))
mergeC_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U5_gga(T18, T60, T20, T22, mergeC_in_gga(T18, .(s(T60), T20), T22))
mergeC_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U6_gga(T18, T20, T22, mergeC_in_gga(T18, .(zero, T20), T22))
mergeC_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_gga(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U7_gga(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → U8_gga(T75, T76, T77, T78, T80, mergeC_in_gga(.(T75, T76), T78, T80))
mergeC_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_gga(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U9_gga(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → U10_gga(T123, T110, T124, T112, T114, mergeC_in_gga(.(s(T123), T110), T112, T114))
mergeC_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U11_gga(T135, T110, T112, T114, mergeC_in_gga(.(s(T135), T110), T112, T114))
U11_gga(T135, T110, T112, T114, mergeC_out_gga(.(s(T135), T110), T112, T114)) → mergeC_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U10_gga(T123, T110, T124, T112, T114, mergeC_out_gga(.(s(T123), T110), T112, T114)) → mergeC_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U8_gga(T75, T76, T77, T78, T80, mergeC_out_gga(.(T75, T76), T78, T80)) → mergeC_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U6_gga(T18, T20, T22, mergeC_out_gga(T18, .(zero, T20), T22)) → mergeC_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U5_gga(T18, T60, T20, T22, mergeC_out_gga(T18, .(s(T60), T20), T22)) → mergeC_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U4_gga(T31, T18, T32, T20, T22, mergeC_out_gga(T18, .(s(T32), T20), T22)) → mergeC_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))
U3_GGA(T31, T18, T32, T20, T22, leA_out_gg(T31, T32)) → MERGEC_IN_GGA(T18, .(s(T32), T20), T22)
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U3_GGA(T31, T18, T32, T20, T22, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(s(T60), T20), T22)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U7_GGA(T75, T76, T77, T78, T80, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T77, T78, T80, gtB_out_gg(T75, T77)) → MERGEC_IN_GGA(.(T75, T76), T78, T80)
MERGEC_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEC_IN_GGA(T18, .(zero, T20), T22)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEC_IN_GGA(.(s(T135), T110), T112, T114)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U9_GGA(T123, T110, T124, T112, T114, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T124, T112, T114, gtB_out_gg(T123, T124)) → MERGEC_IN_GGA(.(s(T123), T110), T112, T114)
leA_in_gg(s(T45), s(T46)) → U1_gg(T45, T46, leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg(zero, s(T53))
leA_in_gg(zero, zero) → leA_out_gg(zero, zero)
gtB_in_gg(s(T93), s(T94)) → U2_gg(T93, T94, gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg(s(T99), zero)
U1_gg(T45, T46, leA_out_gg(T45, T46)) → leA_out_gg(s(T45), s(T46))
U2_gg(T93, T94, gtB_out_gg(T93, T94)) → gtB_out_gg(s(T93), s(T94))
U3_GGA(T18, T32, T20, leA_out_gg) → MERGEC_IN_GGA(T18, .(s(T32), T20))
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → U3_GGA(T18, T32, T20, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEC_IN_GGA(T18, .(s(T60), T20))
MERGEC_IN_GGA(.(T75, T76), .(T77, T78)) → U7_GGA(T75, T76, T78, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T78, gtB_out_gg) → MERGEC_IN_GGA(.(T75, T76), T78)
MERGEC_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEC_IN_GGA(T18, .(zero, T20))
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEC_IN_GGA(.(s(T135), T110), T112)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → U9_GGA(T123, T110, T112, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T112, gtB_out_gg) → MERGEC_IN_GGA(.(s(T123), T110), T112)
leA_in_gg(s(T45), s(T46)) → U1_gg(leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg
leA_in_gg(zero, zero) → leA_out_gg
gtB_in_gg(s(T93), s(T94)) → U2_gg(gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg
U1_gg(leA_out_gg) → leA_out_gg
U2_gg(gtB_out_gg) → gtB_out_gg
leA_in_gg(x0, x1)
gtB_in_gg(x0, x1)
U1_gg(x0)
U2_gg(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U3_GGA(T18, T32, T20, leA_out_gg) → MERGEC_IN_GGA(T18, .(s(T32), T20))
MERGEC_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEC_IN_GGA(T18, .(s(T60), T20))
MERGEC_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEC_IN_GGA(T18, .(zero, T20))
POL(.(x1, x2)) = 1 + x2
POL(MERGEC_IN_GGA(x1, x2)) = x1
POL(U1_gg(x1)) = 0
POL(U2_gg(x1)) = 0
POL(U3_GGA(x1, x2, x3, x4)) = 1 + x1
POL(U7_GGA(x1, x2, x3, x4)) = 1 + x2
POL(U9_GGA(x1, x2, x3, x4)) = 1 + x2
POL(gtB_in_gg(x1, x2)) = 1 + x1 + x2
POL(gtB_out_gg) = 0
POL(leA_in_gg(x1, x2)) = 0
POL(leA_out_gg) = 0
POL(s(x1)) = x1
POL(zero) = 0
MERGEC_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → U3_GGA(T18, T32, T20, leA_in_gg(T31, T32))
MERGEC_IN_GGA(.(T75, T76), .(T77, T78)) → U7_GGA(T75, T76, T78, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T78, gtB_out_gg) → MERGEC_IN_GGA(.(T75, T76), T78)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEC_IN_GGA(.(s(T135), T110), T112)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → U9_GGA(T123, T110, T112, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T112, gtB_out_gg) → MERGEC_IN_GGA(.(s(T123), T110), T112)
leA_in_gg(s(T45), s(T46)) → U1_gg(leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg
leA_in_gg(zero, zero) → leA_out_gg
gtB_in_gg(s(T93), s(T94)) → U2_gg(gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg
U1_gg(leA_out_gg) → leA_out_gg
U2_gg(gtB_out_gg) → gtB_out_gg
leA_in_gg(x0, x1)
gtB_in_gg(x0, x1)
U1_gg(x0)
U2_gg(x0)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78)) → U7_GGA(T75, T76, T78, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T78, gtB_out_gg) → MERGEC_IN_GGA(.(T75, T76), T78)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEC_IN_GGA(.(s(T135), T110), T112)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → U9_GGA(T123, T110, T112, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T112, gtB_out_gg) → MERGEC_IN_GGA(.(s(T123), T110), T112)
leA_in_gg(s(T45), s(T46)) → U1_gg(leA_in_gg(T45, T46))
leA_in_gg(zero, s(T53)) → leA_out_gg
leA_in_gg(zero, zero) → leA_out_gg
gtB_in_gg(s(T93), s(T94)) → U2_gg(gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg
U1_gg(leA_out_gg) → leA_out_gg
U2_gg(gtB_out_gg) → gtB_out_gg
leA_in_gg(x0, x1)
gtB_in_gg(x0, x1)
U1_gg(x0)
U2_gg(x0)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78)) → U7_GGA(T75, T76, T78, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T78, gtB_out_gg) → MERGEC_IN_GGA(.(T75, T76), T78)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEC_IN_GGA(.(s(T135), T110), T112)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → U9_GGA(T123, T110, T112, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T112, gtB_out_gg) → MERGEC_IN_GGA(.(s(T123), T110), T112)
gtB_in_gg(s(T93), s(T94)) → U2_gg(gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg
U2_gg(gtB_out_gg) → gtB_out_gg
leA_in_gg(x0, x1)
gtB_in_gg(x0, x1)
U1_gg(x0)
U2_gg(x0)
leA_in_gg(x0, x1)
U1_gg(x0)
MERGEC_IN_GGA(.(T75, T76), .(T77, T78)) → U7_GGA(T75, T76, T78, gtB_in_gg(T75, T77))
U7_GGA(T75, T76, T78, gtB_out_gg) → MERGEC_IN_GGA(.(T75, T76), T78)
MERGEC_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEC_IN_GGA(.(s(T135), T110), T112)
MERGEC_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → U9_GGA(T123, T110, T112, gtB_in_gg(T123, T124))
U9_GGA(T123, T110, T112, gtB_out_gg) → MERGEC_IN_GGA(.(s(T123), T110), T112)
gtB_in_gg(s(T93), s(T94)) → U2_gg(gtB_in_gg(T93, T94))
gtB_in_gg(s(T99), zero) → gtB_out_gg
U2_gg(gtB_out_gg) → gtB_out_gg
gtB_in_gg(x0, x1)
U2_gg(x0)
From the DPs we obtained the following set of size-change graphs: